NIL 
EVAL-AWAITS 
1 clear(x,z)∧clear(y,z)⊃on(x,y,R(puton(x,y),z));
2 clear(x,y)⊃on(x,T,R(puton(x,T),y));
3 on(y,x,u)⊃z = x∨clear(x,R(puton(y,z),u));
4 clear(x,u)⊃x = z∨clear(x,R(puton(y,z),u));
5 on(x,y,s)⊃z = x∨on(x,y,R(puton(z,u),s));
6 clear(C,S0);
7 clear(B,S0);
8 on(A,T,S0);
9 on(B,T,S0);
10 on(C,A,S0);
11 ¬A = B;
12 ¬B = C;
13 ¬C = A;
14 ¬A = T;
15 ¬B = T;
16 ¬C = T;
17 ¬(on(A,B,x)∧on(B,C,x));
18 on(A,B,z)∧on(B,C,R(puton(x,y),z))⊃A = x;
19 on(B,C,z)∧on(A,B,R(puton(x,y),z))⊃B = x;
20 ¬(on(B,C,R(puton(A,B),x))∧(clear(A,x)∧clear(B,x)));
21 ¬(on(A,B,R(puton(B,C),x))∧(clear(B,x)∧clear(C,x)));
22 ¬(on(B,C,u)∧(on(A,B,R(puton(x,z),u))∧(on(A,B,y)∧on(x,C,y))));
23 on(B,C,R(puton(x,z),R(puton(A,B),y)))∧(clear(A,y)∧clear(B,y))⊃A = x;
24 *DE*
25 on(A,B,s)∧on(B,C,R(puton(x,z),R(puton(y,u),s)))⊃A = y∨A = x;
26 *DE*
27 on(A,B,z)∧on(B,C,R(puton(x,y),z))⊃on(x,T,S0);
28 on(A,B,z)∧on(B,C,R(puton(x,y),z))⊃on(C,x,S0);
29 ¬(on(A,B,y)∧on(B,C,R(puton(B,x),y)));
30 ¬(B = x∧(on(A,B,z)∧on(B,C,R(puton(x,y),z))));
31 ¬(C = x∧(on(A,B,z)∧on(B,C,R(puton(x,y),z))));
32 ¬(on(A,B,y)∧on(B,C,R(puton(T,x),y)));
33 ¬(T = x∧(on(A,B,z)∧on(B,C,R(puton(x,y),z))));
34 on(A,B,R(puton(x,z),R(puton(B,C),y)))∧(clear(B,y)∧clear(C,y))⊃B = x;
35 *DE*
36 on(B,C,s)∧on(A,B,R(puton(x,z),R(puton(y,u),s)))⊃B = y∨B = x;
37 on(B,C,z)∧on(A,B,R(puton(x,y),z))⊃clear(x,S0);
38 on(B,C,z)∧on(A,B,R(puton(x,y),z))⊃on(x,T,S0);
39 ¬(A = x∧(on(B,C,z)∧on(A,B,R(puton(x,y),z))));
40 ¬(on(B,C,y)∧on(A,B,R(puton(C,x),y)));
41 ¬(C = x∧(on(B,C,z)∧on(A,B,R(puton(x,y),z))));
42 ¬(on(B,C,y)∧on(A,B,R(puton(T,x),y)));
43 ¬(T = x∧(on(B,C,z)∧on(A,B,R(puton(x,y),z))));
44 ¬(on(B,C,s)∧(on(A,B,R(puton(x,u),s))∧(on(A,B,z)∧on(x,C,R(puton(B,y),z)))));
45 ¬(on(B,C,s)∧(on(A,B,R(puton(x,u),s))∧(on(A,B,z)∧on(B,C,R(puton(x,y),z)))));
46 ¬(on(B,C,s)∧(on(A,B,R(puton(x,u),s))∧(on(A,B,z)∧on(x,C,R(puton(T,y),z)))));
47 on(y,A,z)∧(on(B,C,R(puton(A,B),R(puton(y,x),z)))∧clear(B,R(puton(y,x),z)))⊃A = x;
48 on(y,B,z)∧(on(B,C,R(puton(A,B),R(puton(y,x),z)))∧clear(A,R(puton(y,x),z)))⊃B = x;
49 on(B,C,R(puton(A,B),R(puton(y,x),z)))∧(clear(A,z)∧clear(B,R(puton(y,x),z)))⊃A = x;
50 on(B,C,R(puton(A,B),R(puton(y,x),z)))∧(clear(B,z)∧clear(A,R(puton(y,x),z)))⊃B = x;
51 ¬(on(B,C,R(puton(A,B),S0))∧clear(A,S0));
52 ¬(on(B,C,y)∧(on(A,B,R(puton(A,x),y))∧on(B,C,R(puton(A,B),S0))));
53 on(y,B,z)∧(on(A,B,R(puton(B,C),R(puton(y,x),z)))∧clear(C,R(puton(y,x),z)))⊃B = x;
54 on(y,C,z)∧(on(A,B,R(puton(B,C),R(puton(y,x),z)))∧clear(B,R(puton(y,x),z)))⊃C = x;
55 on(A,B,R(puton(B,C),R(puton(y,x),z)))∧(clear(B,z)∧clear(C,R(puton(y,x),z)))⊃B = x;
56 on(A,B,R(puton(B,C),R(puton(y,x),z)))∧(clear(C,z)∧clear(B,R(puton(y,x),z)))⊃C = x;
57 ¬on(A,B,R(puton(B,C),S0));
58 on(B,C,R(puton(x,y),R(puton(A,B),S0)))∧clear(A,S0)⊃A = x;
59 on(B,C,R(puton(x,z),R(puton(A,B),y)))∧(clear(A,y)∧clear(B,y))⊃on(x,T,S0);
60 on(B,C,R(puton(x,z),R(puton(A,B),y)))∧(clear(A,y)∧clear(B,y))⊃on(C,x,S0);
61 ¬(on(B,C,R(puton(B,y),R(puton(A,B),x)))∧(clear(A,x)∧clear(B,x)));
62 ¬(B = y∧(on(B,C,R(puton(y,z),R(puton(A,B),x)))∧(clear(A,x)∧clear(B,x))));
63 ¬(C = y∧(on(B,C,R(puton(y,z),R(puton(A,B),x)))∧(clear(A,x)∧clear(B,x))));
64 ¬(on(B,C,R(puton(T,y),R(puton(A,B),x)))∧(clear(A,x)∧clear(B,x)));
65 ¬(T = y∧(on(B,C,R(puton(y,z),R(puton(A,B),x)))∧(clear(A,x)∧clear(B,x))));
66 on(B,C,u)∧(on(A,B,R(puton(A,z),u))∧on(B,C,R(puton(x,y),R(puton(A,B),S0))))⊃A = x;
67 ¬(on(B,C,R(puton(y,z),R(puton(A,B),x)))∧(on(y,B,R(puton(B,C),S0))∧(clear(A,x)∧clear(B,x))));
68 on(A,B,S0)⊃B = A;
69 *DE*
70 *DE*
71 ¬(on(A,B,x)∧(clear(B,x)∧clear(C,x)));
72 on(A,B,s)∧on(B,C,R(puton(x,z),R(puton(y,u),s)))⊃A = y∨on(x,T,S0);
73 on(A,B,s)∧on(B,C,R(puton(x,z),R(puton(y,u),s)))⊃A = y∨on(C,x,S0);
74 on(A,B,u)∧on(B,C,R(puton(x,y),R(puton(B,z),u)))⊃A = x;
75 on(A,B,u)∧on(B,C,R(puton(B,y),R(puton(x,z),u)))⊃A = x;
76 B = y∧(on(A,B,s)∧on(B,C,R(puton(y,z),R(puton(x,u),s))))⊃A = x;
77 C = y∧(on(A,B,s)∧on(B,C,R(puton(y,z),R(puton(x,u),s))))⊃A = x;
78 on(A,B,u)∧on(B,C,R(puton(x,y),R(puton(T,z),u)))⊃A = x;
79 on(A,B,u)∧on(B,C,R(puton(T,y),R(puton(x,z),u)))⊃A = x;
80 T = y∧(on(A,B,s)∧on(B,C,R(puton(y,z),R(puton(x,u),s))))⊃A = x;
81 on(A,B,s)∧(on(B,C,R(puton(y,z),R(puton(x,u),s)))∧on(y,B,R(puton(B,C),S0)))⊃A = x;
82 *DE*
83 *DE*
84 *DE*
85 ¬(on(B,C,x)∧on(A,B,x));
86 on(A,B,u)∧on(B,C,R(puton(x,z),u))⊃T = y∨clear(T,R(puton(x,y),S0));
87 on(A,B,s)∧on(B,C,R(puton(x,u),s))⊃y = x∨on(x,T,R(puton(y,z),S0));
88 on(A,B,S0)∧(on(B,B,z)∧on(B,C,R(puton(x,y),z)))⊃on(x,T,S0);
89 on(A,B,u)∧on(B,C,R(puton(x,z),u))⊃y = x∨clear(x,R(puton(C,y),S0));
90 on(A,B,s)∧on(B,C,R(puton(x,u),s))⊃C = y∨on(C,x,R(puton(y,z),S0));
91 on(A,B,S0)∧(on(B,B,z)∧on(B,C,R(puton(x,y),z)))⊃on(C,x,S0);
92 ¬(on(A,B,S0)∧(on(B,B,y)∧on(B,C,R(puton(B,x),y))));
93 ¬(on(A,B,S0)∧(on(A,B,y)∧on(A,C,R(puton(B,x),y))));
94 on(y,x,z)∧(on(A,B,s)∧on(B,C,R(puton(x,u),s)))⊃clear(x,R(puton(y,B),z));
95 on(A,B,s)∧(on(B,C,R(puton(y,u),s))∧clear(B,z))⊃clear(B,R(puton(x,y),z));
96 on(x,y,u)∧(on(A,B,x1)∧on(B,C,R(puton(x,s),x1)))⊃on(x,y,R(puton(B,z),u));
97 ¬(on(A,B,S0)∧(on(A,B,y)∧on(B,C,R(puton(A,x),y))));
98 ¬(B = x∧(on(A,B,S0)∧(on(B,B,z)∧on(B,C,R(puton(x,y),z)))));
99 ¬(B = x∧(on(A,B,S0)∧(on(A,B,z)∧on(A,C,R(puton(x,y),z)))));
100 on(y,x,z)∧(on(A,B,s)∧on(B,C,R(puton(x,u),s)))⊃clear(x,R(puton(y,C),z));
101 on(A,B,s)∧(on(B,C,R(puton(y,u),s))∧clear(C,z))⊃clear(C,R(puton(x,y),z));
102 on(x,y,u)∧(on(A,B,x1)∧on(B,C,R(puton(x,s),x1)))⊃on(x,y,R(puton(C,z),u));
103 ¬(C = x∧(on(A,B,S0)∧(on(B,B,z)∧on(B,C,R(puton(x,y),z)))));
104 ¬(C = x∧(on(A,B,S0)∧(on(A,B,z)∧on(A,C,R(puton(x,y),z)))));
105 ¬(on(A,B,S0)∧(on(B,B,y)∧on(B,C,R(puton(T,x),y))));
106 ¬(on(A,B,S0)∧(on(A,B,y)∧on(A,C,R(puton(T,x),y))));
107 ¬(on(A,B,z)∧(on(A,B,s)∧(on(B,C,R(puton(A,u),s))∧on(B,C,R(puton(T,x),R(puton(B,y),z))))));
108 ¬(on(A,B,z)∧(on(A,B,s)∧(on(B,C,R(puton(A,u),s))∧on(B,C,R(puton(T,x),R(puton(C,y),z))))));
109 on(y,x,z)∧(on(A,B,s)∧on(B,C,R(puton(x,u),s)))⊃clear(x,R(puton(y,T),z));
110 on(A,B,s)∧(on(B,C,R(puton(y,u),s))∧clear(T,z))⊃clear(T,R(puton(x,y),z));
111 on(x,y,u)∧(on(A,B,x1)∧on(B,C,R(puton(x,s),x1)))⊃on(x,y,R(puton(T,z),u));
112 ¬(T = x∧(on(A,B,S0)∧(on(B,B,z)∧on(B,C,R(puton(x,y),z)))));
113 ¬(T = x∧(on(A,B,S0)∧(on(A,B,z)∧on(A,C,R(puton(x,y),z)))));
114 on(A,B,R(puton(x,y),R(puton(B,C),S0)))⊃B = x;
115 on(A,B,R(puton(x,z),R(puton(B,C),y)))∧(clear(B,y)∧clear(C,y))⊃clear(x,S0);
116 on(A,B,R(puton(x,z),R(puton(B,C),y)))∧(clear(B,y)∧clear(C,y))⊃on(x,T,S0);
117 ¬(A = y∧(on(A,B,R(puton(y,z),R(puton(B,C),x)))∧(clear(B,x)∧clear(C,x))));
118 ¬(on(A,B,R(puton(C,y),R(puton(B,C),x)))∧(clear(B,x)∧clear(C,x)));
119 ¬(C = y∧(on(A,B,R(puton(y,z),R(puton(B,C),x)))∧(clear(B,x)∧clear(C,x))));
120 ¬(on(A,B,R(puton(T,y),R(puton(B,C),x)))∧(clear(B,x)∧clear(C,x)));
121 ¬(T = y∧(on(A,B,R(puton(y,z),R(puton(B,C),x)))∧(clear(B,x)∧clear(C,x))));
122 ¬(on(A,B,R(puton(y,z),R(puton(B,C),x)))∧(on(A,y,R(puton(B,C),S0))∧(clear(B,x)∧clear(C,x))));
123 on(B,C,S0)∧clear(A,S0)⊃B = A;
124 *DE*
125 *DE*
126 ¬(on(B,C,x)∧(clear(A,x)∧clear(B,x)));
127 on(B,C,s)∧on(A,B,R(puton(x,z),R(puton(y,u),s)))⊃B = y∨clear(x,S0);
128 on(B,C,s)∧on(A,B,R(puton(x,z),R(puton(y,u),s)))⊃B = y∨on(x,T,S0);
129 A = y∧(on(B,C,s)∧on(A,B,R(puton(y,z),R(puton(x,u),s))))⊃B = x;
130 on(B,C,u)∧on(A,B,R(puton(x,y),R(puton(C,z),u)))⊃B = x;
131 on(B,C,u)∧on(A,B,R(puton(C,y),R(puton(x,z),u)))⊃B = x;
132 C = y∧(on(B,C,s)∧on(A,B,R(puton(y,z),R(puton(x,u),s))))⊃B = x;
133 on(B,C,u)∧on(A,B,R(puton(x,y),R(puton(T,z),u)))⊃B = x;
134 on(B,C,u)∧on(A,B,R(puton(T,y),R(puton(x,z),u)))⊃B = x;
135 T = y∧(on(B,C,s)∧on(A,B,R(puton(y,z),R(puton(x,u),s))))⊃B = x;
136 on(B,C,s)∧(on(A,B,R(puton(y,z),R(puton(x,u),s)))∧on(A,y,R(puton(B,C),S0)))⊃B = x;
137 on(B,C,u)∧(on(A,B,R(puton(x,z),u))∧clear(y,S0))⊃on(x,y,R(puton(x,y),S0));
138 on(B,C,u)∧(on(A,B,R(puton(y,z),u))∧clear(x,S0))⊃on(x,y,R(puton(x,y),S0));
139 on(B,C,z)∧on(A,B,R(puton(x,y),z))⊃on(x,T,R(puton(x,T),S0));
140 on(B,C,s)∧on(A,B,R(puton(x,u),s))⊃z = x∨clear(x,R(puton(y,z),S0));
141 on(B,C,u)∧(on(A,B,R(puton(A,z),u))∧on(B,C,R(puton(x,y),R(puton(A,B),S0))))⊃on(x,T,S0);
142 on(B,C,u)∧(on(A,B,R(puton(A,z),u))∧on(B,C,R(puton(x,y),R(puton(A,B),S0))))⊃on(C,x,S0);
NIL 
EVAL-AWAITS